IrrelevantRecordMatching.agda:12,12-18
Cannot pattern match against irrelevant argument of type Prod A A
when checking that the pattern a , a' has type Prod A A
